----------- MODULE run_tas -----------

EXTENDS var_module, tas

INSTANCE run_module

Invariant == [] Inv(Etat)


===========================================

